g:IGroup, a, b:|g|. (a * ((~(a)) * b)) = b & ((~(a)) * (a * b)) = b 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	t  T, x:A. B(x), P  Q, P  Q, P  Q, x f y, P & Q, IMonoid, IGroup
Lemmas	igrp wf, grp car wf, mon ident, grp inverse, grp op wf, grp inv wf, mon assoc